i, j:, n:. (((i rem n)+(j rem n)) rem n) = ((i+j) rem n) 

latex

Up	int 2, int 2
Definitions	t  T, x:A. B(x), P & Q, P  Q, P  Q, False, P  Q, A, a  b  T , , A  B, , , S  T
Lemmas	nat wf, nat plus wf, div rem sum, add functionality wrt eq, nat plus inc int nzero, divide wfa, rem invariant, le wf, rem bounds 1, add functionality wrt le, div bounds 1